
; Copyright (c) 2015 Microsoft Corporation
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const r1 Real)
(declare-const r2 Real)
(set-option :pp.flat-assoc false)

(simplify (* 2 (* a (* b (* c d))))
                 :flat true)
(simplify (* 2 (* a (* b (* c d))))
                 :flat false)

(simplify (* a b (* c d)))
(simplify (* a b (* c d))
                 :flat false)
(simplify (* 2 (+ a b 1))
                 :flat true)

(simplify (+ 1 2))
(simplify (- 1))
(simplify (+ (- 2) 2))
(simplify (+ a 1 2))
(simplify (+ a 1 a 2))
(simplify (+ 1 a))
(simplify (+ 1 a b))
(simplify (+ 1 a b (* (- 1) a) c 2 c))
(simplify (+ (+ a b) a))
(simplify (+ (+ a b) a)
                 :flat false)
(simplify (* 2 3))
(simplify (* a b 0 c))
(simplify (* 0.5 2.0 r1))
(simplify (* 2 (* 3 a))
                 :flat false)
(simplify (* 2 (+ a b 1))
                 :flat false)
(simplify (* 2 (+ a b 1))
                 :flat true)
(simplify (* 2 (* a 3))
                 :flat false)
(simplify (* 2 (* a (* 2 b c)))
                 :flat false)
(simplify (* 2 (* a (* 2 b c)))
                 :flat true)
(simplify (* 2 (* a (* b (* c d))))
                 :flat true)
(simplify (* 2 (* a (* b (* c d))))
                 :flat false)
(simplify (* (+ a b) (+ c d)))
(simplify (* (+ a b) (+ c d))
                 :som true)
(simplify (* (+ a b) (+ a b))
                 :som true)
(simplify (* (+ a b) (+ a b) (+ a b))
                 :som true)
(simplify (* (+ a b) (+ a b) (+ a b) (+ a b))
                 :som true)
(simplify (* (+ 2 a b) (+ c d) (+ a c))
                 :som true)



